Nuprl Definition : firstn
11,40
postcript
pdf
firstn(
n
;
as
)
== rec-case(
as
) of [] => [] |
a
::
as'
=>
.if 0 <z
n
then cons(
a
; firstn((
n
- 1);
as'
)) else [] fi
(recursive)
latex
Definitions
Y
,
x
.
A
(
x
)
,
rec-case(
a
) of [] =>
s
|
x
::
y
=>
z
.
t
(
x
;
y
;
z
)
,
if
b
then
t
else
f
fi
,
i
<z
j
,
cons(
car
;
cdr
)
,
f
(
a
)
,
n
-
m
,
#$n
,
[]
FDL editor aliases
firstn
origin
x.A(x), rec-case(a) of [] => s | x::y => z.t(x;y;z), if b then t else f fi , i <z j, cons(car; cdr), f(a), n - m, #$n, []